|
Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression. == History == Alonzo Church invented the lambda calculus in the 1930s, originally to provide a new and simpler basis for mathematics.〔A. Church, "A set of postulates for the foundation of logic", ''Annals of Mathematics'', Series 2, 33:346–366 (1932).〕〔For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).〕 However soon after inventing it major logic problems were identified with the definition of the lambda abstraction. Haskell Curry studied of illative (deductive) combinatory logic in 1941. Combinatory logic is closely related to lambda calculus. The Kleene–Rosser paradox is an implementation of Richard's paradox in Combinatory logic. Combinatory Logic is closely related to Lambda Calculus. Haskell Curry found that the key step in this paradox could be used to implement the simpler Curry's Paradox. The existence of this paradox meant that the Combinatory Logic, and lambda calculus, could not be both consistent and complete as a deductive system.〔 The Inconsistency of Certain Formal Logic Haskell B. Curry The Journal of Symbolic Logic Vol. 7, No. 3 (Sep., 1942), pp. 115-117 Published by: Association for Symbolic Logic Article Stable URL: http://www.jstor.org/stable/2269292 〕 Later the Lambda Calculus was resurrected as a definition of a programming language. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Deductive lambda calculus」の詳細全文を読む スポンサード リンク
|